COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00009 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.turn off "$"
.cb ON THE MODEL THEORY OF KNOWLEDGE

.ITEM←0
.BB "#. Introduction."

	The need to represent information about who knows what in
intelligent computer programs was the original motivation for this work.
For example, a program that plans trips must know that travel agents know
who knows the availability of rooms in hotels.  An early problem is how to
represent what people know about other people's knowledge of facts, and
even the knowledge of propositions treated in this paper presented some
problems that were not treated in previous literature.

	We started with the following well known puzzle of the three wise
men:  %2A king wishing to know which of his three wise men is the wisest,
paints a white spot on each of their foreheads, tells them at least one
spot is white, and asks each to determine the color of his spot.  After a
while the smartest announces that his spot is white reasoning as follows:
"Suppose my spot were black.  The second wisest of us would then see a
black and a white and would reason that if his spot were black, the
dumbest would see two black spots and would conclude that his spot is
white on the basis of the king's assurance.  He would have announced it by
now, so my spot must be white."%1

	In formalizing the puzzle, we don't wish to try to formalize
reasoning about how fast other people reason.  Therefore, we will imagine
that either the king asks the wise men in sequence whether they
know the colors of their spots or that he asks synchronously, "Do you
know the color of your spot" getting a chorus of noes.  He asks it
again with the same result, but on the third asking, they answer that
their spots are white.  Needless to say, we are also not formalizing any
notion of relative wisdom.

	We start with a general set of axioms for knowledge based on
the notation, axioms, and inference rules of propositional calculus
supplemented by the
notation %2S*p%1 standing for, "Person %2S%1 knows proposition %2p%1."  Thus
%2W3*W2*¬(W1*p1)%1 can stand for, "The third wise man knows that the second
wise man knows that the first wise man does not know that the first
wise man's spot is white".

	We use axiom schemata with subscripted S's as person variables,
subscripted p's and q's as propositional variables, and a special person
constant called "any fool" and denoted by 0.  It is convenient to
introduce "any fool" because whatever he knows, every one knows that
everyone else knows.  "Any fool" is especially useful when an event occurs
in front of all the knowers, and we need sentences like, "%2S1%1 knows
that %2S2%1 knows that %2S3%1 knows etc.".  Here are the schemata:

K0:	%2S*p ⊃ p%1; What a person knows is true.

K1:	%20*(S*p ⊃ p)%1; Any fool knows that what a person knows is true.

K2:	%20*(0*p ⊃ 0*S*p)%1; What any fool knows, any fool knows everyone knows,
and any fool knows that.

K3:	%20*(S*p ∧ S*(p ⊃ q) ⊃ S*q)%1; Any fool knows everyone can do modus ponens.

	There are two optional schemata K4 and K5:

K4:	%20*(S*p ⊃ S*S*p)%1; Any fool knows that what someone knows, he knows
he knows.

K5:	%20*(¬S*p ⊃ S*¬S*p)%1; Any fool knows that what some doesn't know he
knows he doesn't know.

	If there is only one person ⊗S, the system is equivalent to a
system of modal logic.  Axioms K1-K3 give a system equivalent to what
Hughes and Cresswell call T, and K4 and K5 give the modal systems S4 and
S5 respectively.  We call K4 and K5 the introspective schemata.

	It is convenient to write ⊗Sα$p as an abbreviation for %2S*p_∨_S*¬p%1;
it may be read, "⊗S knows whether %2p%1".

	On the basis of these schemata we may axiomatize the wise man
problem as follows:

A0:	%2p1 ∧ p2 ∧ p3%1

A1:	%20*(p1 ∨ p2 ∨ p3)%1

A2:	%20*(W1α$p2 ∧ W1α$p3 ∧ W2α$p1 ∧ W2α$p3 ∧ W3α$p1 ∧ W2α$p2)%1

A2:	%20*(W2α$W1*p1)%1

A3:	%20*(W3α$W2*p2)%1

A4:	%2¬W1α$p1%1

A5:	%2¬W2α$p2%1

	From K0-K3 and A1-A5 it is possible to prove %2W3*p3%1.
A0 is not used in the proof.  In some sense A4 and A5 should not
be required.  Looking at the problem sequentially, it should follow
that ⊗W1 does not know ⊗p1 initially, and that even knowing that,
⊗W2 doesn't know ⊗p2. 

	In order to proceed further with the problem, model theoretic
semantics is necessary.